| Definitions | t  T,  b, x:A  B(x),  x:A. B(x), {x:A| B(x)} , E(X), let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), P   Q, ES, AbsInterface(A), e c e', no_repeats(T;l), x:A  B(x), left + right, P  Q, (e < e'), False,  A, Top, prior-f-fixedpoints(e), Dec(P), (e <loc e'), e loc e' ,  x:A. B(x), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e),  , a < b, {T}, n+m,  , A B, Type,  , Void,  , S  T, #$n, n - m,  , e < e', (x l), SWellFounded(R(x;y)), EState(T), Id, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, constant_function(f;A;B), pred!(e;e'),   x,y. t(x;y), <a, b>, pred(e), first(e), x. t(x), P & Q, i  j , Outcome, -n, f(a), E, s = t, prior(X), e  X, [], P  Q, P Q, [car / cdr], A c B, ff, b, tt, as @ bs, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p q, p q, p q, X(e), l_disjoint(T;l1;l2), A List , sender(e), ||as||, l[i], |g|, e(e1,e2].P(e), @e(x v), (last change to x before e), pred(e), loc(e), kind(e), True,  T, source(l), destination(l), es-init(es;e), s ~ t, SQType(T), isrcv(e), es-first-from(es;e;l;tg), isrcv(k), Atom$n, lastchange(x;e), f**(e) |
| Lemmas | es-fix-equal, es-fix-causle, es-prior-fixedpoints-fix, es-fix wf2, es-locl transitivity2, es-locl irreflexivity, es-causle-le, iff wf, rev implies wf, es-isrcv-loc, es-le-loc, true wf, squash wf, es-loc wf, es-loc-pred, es-locl-iff, es-interface-subtype rel, es-locl wf, es-prior-interface-locl, es-causle transitivity, es-causle weakening locl, es-le weakening, es-prior-fixedpoints-causle, length wf1, select wf, es-prior-interface-causl, no repeats-append, l disjoint singleton, es-interface-val wf2, es-prior-fixedpoints wf, es-interface-val wf, assert-es-eq-E-2, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-is-interface wf, es-prior-interface wf, bnot wf, no repeats cons, no repeats nil, not functionality wrt iff, nil member, l member wf, false wf, ge wf, nat properties, event system wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, val-axiom wf, qle wf, cless wf, bool wf, Knd wf, kindcase wf, constant function wf, assert wf, not wf, loc wf, pred! wf, strongwellfounded wf, rationals wf, Id wf, EState wf, top wf, es-interface wf, es-causle wf, es-causl-swellfnd, nat ind tp, no repeats wf, guard wf, es-causl wf, le wf, nat wf, decidable es-E-equal, es-E-interface-subtype rel, member wf, es-E wf, es-E-interface wf, subtype rel wf |